| Definitions | s = t, t  T, x:A  B(x),  x:A. B(x), ES, a:A fp B(a), x:A  B(x), Type, EqDecider(T), Unit, left + right, IdLnk, Id, EOrderAxioms(E; pred?; info), f(a), EState(T), Knd,   x. t(x), x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List,  ,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, P   Q,  ,  b, constant_function(f;A;B), P & Q, Top, strong-subtype(A;B), AbsInterface(A), E(X), let x,y = A in B(x;y), (e < e'), {x:A| B(x)} , chain_master(), chain_config(), E, t.1, P  Q, P Q, f  g, f(x)?z, loc(e), vartype(i;x), state@i, State(ds), State(ds), e  X,  , loc(e), kind(e), SWellFounded(R(x;y)), pred!(e;e'), Void,  x:A.B(x), S T, suptype(S; T), first(e),  A, <a, b>, pred(e), x.A(x), (e <loc e'), A B, #$n,  , Atom$n, |g|, cmseq-num(x), cmseq-to(x), cmseq-from(x), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , cmseq?(x), False, A c B, tt, inr x , ff, inl x , True, {i..j }, a < b, cmconfig-list(x), l[i], n - m, cmconfig?(x), ||as||, i j < k, -n, n+m,  x:A. B(x), last(L), null(as), i  j , hd(l), X(e), chain_config_ind(x;head;tail;id.pred(id);id,num.succ(id;num)), "$token", Atom, t.2, Outcome, let x = a in b(x), config-antecedent(es;Master;Config;c) |
| Lemmas | es-causl wf, es-locl wf, es-interface-val wf2, cmconfig? wf, es-interface-val wf, let wf, cmseq? wf, pi1 wf, pi2 wf, chain config ind wf, ge wf, hd wf, null wf3, last wf, int seg wf, length wf1, select wf, cmconfig-list wf, true wf, false wf, bfalse wf, btrue wf, cmseq-to wf, es-loc wf, cmseq-from wf, cmseq-num wf, le wf, es-interface wf, chain config wf, kind wf, loc wf, not wf, first wf, pred! wf, strongwellfounded wf, es-is-interface wf, chain master wf, es-E wf, es-E-interface wf, member wf, top wf, constant function wf, assert wf, bool wf, qle wf, cless wf, val-axiom wf, rationals wf, nat wf, Msg wf, kindcase wf, Knd wf, EState wf, EOrderAxioms wf, Id wf, IdLnk wf, unit wf, deq wf, event system wf, subtype rel wf |
c:(E(Config)